Left Termination of the query pattern w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

a :- b.
a :- e.
b :- c.
c :- d.
d :- b.
e :- f.
f :- g.
g :- e.

Queries:

a().

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

A_IN_ → U1_1(b_in_)
A_IN_ → B_IN_
B_IN_ → U3_1(c_in_)
B_IN_ → C_IN_
C_IN_ → U4_1(d_in_)
C_IN_ → D_IN_
D_IN_ → U5_1(b_in_)
D_IN_ → B_IN_
A_IN_ → U2_1(e_in_)
A_IN_ → E_IN_
E_IN_ → U6_1(f_in_)
E_IN_ → F_IN_
F_IN_ → U7_1(g_in_)
F_IN_ → G_IN_
G_IN_ → U8_1(e_in_)
G_IN_ → E_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

A_IN_ → U1_1(b_in_)
A_IN_ → B_IN_
B_IN_ → U3_1(c_in_)
B_IN_ → C_IN_
C_IN_ → U4_1(d_in_)
C_IN_ → D_IN_
D_IN_ → U5_1(b_in_)
D_IN_ → B_IN_
A_IN_ → U2_1(e_in_)
A_IN_ → E_IN_
E_IN_ → U6_1(f_in_)
E_IN_ → F_IN_
F_IN_ → U7_1(g_in_)
F_IN_ → G_IN_
G_IN_ → U8_1(e_in_)
G_IN_ → E_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 10 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

The TRS R consists of the following rules:none


s = F_IN_ evaluates to t =F_IN_

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

F_IN_ → G_IN_
with rule F_IN_ → G_IN_ at position [] and matcher [ ]

G_IN_ → E_IN_
with rule G_IN_ → E_IN_ at position [] and matcher [ ]

E_IN_ → F_IN_
with rule E_IN_ → F_IN_

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

The TRS R consists of the following rules:none


s = D_IN_ evaluates to t =D_IN_

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

D_IN_ → B_IN_
with rule D_IN_ → B_IN_ at position [] and matcher [ ]

B_IN_ → C_IN_
with rule B_IN_ → C_IN_ at position [] and matcher [ ]

C_IN_ → D_IN_
with rule C_IN_ → D_IN_

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.

Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

A_IN_ → U1_1(b_in_)
A_IN_ → B_IN_
B_IN_ → U3_1(c_in_)
B_IN_ → C_IN_
C_IN_ → U4_1(d_in_)
C_IN_ → D_IN_
D_IN_ → U5_1(b_in_)
D_IN_ → B_IN_
A_IN_ → U2_1(e_in_)
A_IN_ → E_IN_
E_IN_ → U6_1(f_in_)
E_IN_ → F_IN_
F_IN_ → U7_1(g_in_)
F_IN_ → G_IN_
G_IN_ → U8_1(e_in_)
G_IN_ → E_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

A_IN_ → U1_1(b_in_)
A_IN_ → B_IN_
B_IN_ → U3_1(c_in_)
B_IN_ → C_IN_
C_IN_ → U4_1(d_in_)
C_IN_ → D_IN_
D_IN_ → U5_1(b_in_)
D_IN_ → B_IN_
A_IN_ → U2_1(e_in_)
A_IN_ → E_IN_
E_IN_ → U6_1(f_in_)
E_IN_ → F_IN_
F_IN_ → U7_1(g_in_)
F_IN_ → G_IN_
G_IN_ → U8_1(e_in_)
G_IN_ → E_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 2 SCCs with 10 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

E_IN_ → F_IN_
F_IN_ → G_IN_
G_IN_ → E_IN_

The TRS R consists of the following rules:none


s = F_IN_ evaluates to t =F_IN_

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

F_IN_ → G_IN_
with rule F_IN_ → G_IN_ at position [] and matcher [ ]

G_IN_ → E_IN_
with rule G_IN_ → E_IN_ at position [] and matcher [ ]

E_IN_ → F_IN_
with rule E_IN_ → F_IN_

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

The TRS R consists of the following rules:

a_in_ → U1_(b_in_)
b_in_ → U3_(c_in_)
c_in_ → U4_(d_in_)
d_in_ → U5_(b_in_)
U5_(b_out_) → d_out_
U4_(d_out_) → c_out_
U3_(c_out_) → b_out_
U1_(b_out_) → a_out_
a_in_ → U2_(e_in_)
e_in_ → U6_(f_in_)
f_in_ → U7_(g_in_)
g_in_ → U8_(e_in_)
U8_(e_out_) → g_out_
U7_(g_out_) → f_out_
U6_(f_out_) → e_out_
U2_(e_out_) → a_out_

Pi is empty.
We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

C_IN_ → D_IN_
B_IN_ → C_IN_
D_IN_ → B_IN_

The TRS R consists of the following rules:none


s = D_IN_ evaluates to t =D_IN_

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

D_IN_ → B_IN_
with rule D_IN_ → B_IN_ at position [] and matcher [ ]

B_IN_ → C_IN_
with rule B_IN_ → C_IN_ at position [] and matcher [ ]

C_IN_ → D_IN_
with rule C_IN_ → D_IN_

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.